L:Dsys List.
(A,BL.A || B)
 (M:Dsys. (BL. interface-compatible(B;M))  interface-compatible((L);M)) 

latex

Definitions	(x  l), (L), x. t(x), (x,yL.P(x;y)), x,y. t(x;y), Prop, A || B, MsgA, {T}, P & Q, P  Q, x:A. B(x), t  T, xL. P(x), interface-compatible(A;B), Dsys
Lemmas	interface-compatible-join-list, interface-compatible-symmetry, dsys-join-list-property, dsys wf, m-sys-compatible wf, pairwise wf, interface-compatible wf, l all wf, l member wf